Theorem a14b 820

Description: An identity law for the non-logical predicate.

Assertion

Ref	Expression
a14b	|- (x = y -> (z e. x <-> z e. y))

Proof of Theorem a14b

Step	Hyp	Ref	Expression
1		ax-14 805	. 2 |- (x = y -> (z e. x -> z e. y))
2		ax-14 805	. . 3 |- (y = x -> (z e. y -> z e. x))
3	2	eqcoms 813	. 2 |- (x = y -> (z e. y -> z e. x))
4	1, 3	impbid 397	1 |- (x = y -> (z e. x <-> z e. y))

Syntax hints:   -> wi 2   <-> wb 127   = weq 797   e. wel 803

This theorem is referenced by:  ddeel2 1004  axun 1081  axac 1085  zfext2 1087  bm1.1 1088  axrep2 1474  zfrep2 1475  bm1.3ii 1481  nalset 1482  aceq0 3553  nd2 3733  nd3 3734  axrepndlem2 3739  axunndlem1 3741  axunnd 3742  axpowndlem2 3744  axpowndlem3 3745  axpowndlem4 3746  axpownd 3747  axregndlem2 3749  axregnd 3750  axinfndlem1 3751  axacndlem4 3756  axacndlem5 3757  axacnd 3758  zfcndrep 3760  zfcndun 3761  zfcndac 3765

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-gen 677  ax-8 798  ax-9 799  ax-12 802  ax-14 805

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679

metamath.org