Theorem a13b 819

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

Assertion

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

Proof of Theorem a13b

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

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

This theorem is referenced by:  cleljust 985  ddeel1 1003  ax15 1006  axun 1081  axpow 1082  axinf 1084  axac 1085  nalset 1482  aceq0 3553  nd1 3732  axextnd 3737  axrepndlem1 3738  axrepndlem2 3739  axunndlem1 3741  axunnd 3742  axpowndlem2 3744  axpowndlem3 3745  axpowndlem4 3746  axregndlem1 3748  axregndlem2 3749  axregnd 3750  axinfnd 3752  axacndlem5 3757  axacnd 3758  zfcndun 3761  zfcndpow 3762  zfcndinf 3764  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-13 804

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

metamath.org