Theorem elequ2 2123

Description: An identity law for the non-logical predicate. (Contributed by NM, 21-Jun-1993.)

Assertion

Ref	Expression
elequ2	⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))

Proof of Theorem elequ2

Step	Hyp	Ref	Expression
1		ax9 2122	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
2		ax9 2122	. . 3 ⊢ (𝑦 = 𝑥 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥))
3	2	equcoms 2019	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥))
4	1, 3	impbid 212	1 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))

Syntax hints:   → wi 4   ↔ wb 206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778

This theorem is referenced by:  elequ2g  2124  elsb2  2125  elequ12  2126  ax12wdemo  2135  dveel2  2470  axextg  2713  axextmo  2715  eleq2w  2828  nfcvf  2938  unissb  4963  dftr2c  5286  axrep1  5304  axreplem  5305  axrep4  5308  axsepg  5318  bm1.3ii  5320  nalset  5331  fv3  6938  zfun  7771  tz7.48lem  8497  coflton  8727  aceq1  10186  aceq0  10187  aceq2  10188  dfac2a  10199  kmlem4  10223  axdc3lem2  10520  zfac  10529  nd2  10657  nd3  10658  axrepndlem2  10662  axunndlem1  10664  axunnd  10665  axpowndlem2  10667  axpowndlem3  10668  axpowndlem4  10669  axpownd  10670  axregndlem2  10672  axregnd  10673  axinfndlem1  10674  axacndlem5  10680  zfcndrep  10683  zfcndun  10684  zfcndac  10688  axgroth4  10901  nqereu  10998  mdetunilem9  22647  neiptopnei  23161  2ndc1stc  23480  restlly  23512  kqt0lem  23765  regr1lem2  23769  nrmr0reg  23778  hauspwpwf1  24016  dya2iocuni  34248  axsepg2  35058  axsepg2ALT  35059  axnulg  35068  erdsze  35170  untsucf  35672  untangtr  35676  dfon2lem3  35749  dfon2lem6  35752  dfon2lem7  35753  dfon2lem8  35754  dfon2  35756  axextbdist  35764  distel  35767  axextndbi  35768  fness  36315  fneref  36316  bj-axc14nf  36821  bj-bm1.3ii  37030  matunitlindflem1  37576  prtlem13  38824  prtlem15  38831  prtlem17  38832  dveel2ALT  38895  ax12el  38898  aomclem8  43018  unielss  43179  elintima  43615  mnuprdlem3  44243  ismnushort  44270  axc11next  44375  setcthin  48722