Theorem elequ2 2126

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 2125	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
2		ax9 2125	. . 3 ⊢ (𝑦 = 𝑥 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥))
3	2	equcoms 2021	. 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 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121

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

This theorem is referenced by:  elequ2g  2127  elsb2  2128  elequ12  2129  ax12wdemo  2138  dveel2  2462  axextg  2705  axextmo  2707  eleq2w  2815  nfcvf  2921  sbralie  3318  unissb  4889  dftr2c  5199  axrep1  5216  axreplem  5217  axrep4OLD  5222  axsepg  5233  bm1.3iiOLD  5238  nalset  5249  fv3  6840  zfun  7669  tz7.48lem  8360  coflton  8586  aceq1  10008  aceq0  10009  aceq2  10010  dfac2a  10021  kmlem4  10045  axdc3lem2  10342  zfac  10351  nd2  10479  nd3  10480  axrepndlem2  10484  axunndlem1  10486  axunnd  10487  axpowndlem2  10489  axpowndlem3  10490  axpowndlem4  10491  axpownd  10492  axregndlem2  10494  axregnd  10495  axinfndlem1  10496  axacndlem5  10502  zfcndrep  10505  zfcndun  10506  zfcndac  10510  axgroth4  10723  nqereu  10820  mdetunilem9  22535  neiptopnei  23047  2ndc1stc  23366  restlly  23398  kqt0lem  23651  regr1lem2  23655  nrmr0reg  23664  hauspwpwf1  23902  constrcbvlem  33768  dya2iocuni  34296  axsepg2  35094  axsepg2ALT  35095  axnulg  35119  erdsze  35246  untsucf  35754  untangtr  35758  dfon2lem3  35827  dfon2lem6  35830  dfon2lem7  35831  dfon2lem8  35832  dfon2  35834  axextbdist  35842  distel  35845  axextndbi  35846  fness  36393  fneref  36394  bj-axc14nf  36899  bj-bm1.3ii  37108  matunitlindflem1  37666  prtlem13  38977  prtlem15  38984  prtlem17  38985  dveel2ALT  39048  ax12el  39051  aomclem8  43164  unielss  43321  elintima  43756  mnuprdlem3  44377  ismnushort  44404  axc11next  44509  setcthin  49576