abbi - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > abbi		Unicode version

Theorem abbi 2463

Description: Equivalent wff's correspond to equal class abstractions. (Contributed by NM, 25-Nov-2013.) (Revised by Mario Carneiro, 11-Aug-2016.)

**Assertion**
Ref	Expression
abbi

Proof of Theorem abbi Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfcleq 2347	. 2
2		nfsab1 2343	. . . 4
3		nfsab1 2343	. . . 4
4	2, 3	nfbi 1834	. . 3
5		nfv 1619	. . 3
6		df-clab 2340	. . . . 5
7		sbequ12r 1920	. . . . 5
8	6, 7	syl5bb 248	. . . 4
9		df-clab 2340	. . . . 5
10		sbequ12r 1920	. . . . 5
11	9, 10	syl5bb 248	. . . 4
12	8, 11	bibi12d 312	. . 3
13	4, 5, 12	cbval 1984	. 2
14	1, 13	bitr2i 241	1

Colors of variables: wff setvar class

Syntax hints:

wb 176

wal 1540

wceq 1642

wsb 1648

wcel 1710

cab 2339

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-6 1729 ax-7 1734 ax-11 1746 ax-12 1925 ax-ext 2334

This theorem depends on definitions: df-bi 177 df-an 360 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-clab 2340 df-cleq 2346

This theorem is referenced by: abbii 2465 abbid 2466 rabbi 2789 dfeu2 4333 dfiota2 4340 iotabi 4348 uniabio 4349 iotanul 4354