Theorem eleq2w 2896

Description: Weaker version of eleq2 2901 (but more general than elequ2 2129) not depending on ax-ext 2793 nor df-cleq 2814. (Contributed by BJ, 29-Sep-2019.)

Assertion

Ref	Expression
eleq2w	⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦))

Proof of Theorem eleq2w

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elequ2 2129	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))
2	1	anbi2d 630	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ (𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦)))
3	2	exbidv 1922	. 2 ⊢ (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦)))
4		dfclel 2894	. 2 ⊢ (𝐴 ∈ 𝑥 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥))
5		dfclel 2894	. 2 ⊢ (𝐴 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦))
6	3, 4, 5	3bitr4g 316	1 ⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537  ∃wex 1780   ∈ wcel 2114

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 1970  ax-7 2015  ax-8 2116  ax-9 2124

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-clel 2893

This theorem is referenced by:  eluniab  4853  elintab  4887  cantnflem1c  9150  tcrank  9313  isf32lem2  9776  sadcp1  15804  subgacs  18313  nsgacs  18314  sdrgacs  19580  lssacs  19739  elcls3  21691  conncompconn  22040  1stcfb  22053  dfac14lem  22225  r0cld  22346  uffix  22529  flftg  22604  tgpconncompeqg  22720  wilth  25648  tghilberti2  26424  umgr2edgneu  26996  uspgredg2v  27006  usgredgleordALT  27016  nbusgrf1o  27153  vtxdushgrfvedglem  27271  ddemeas  31495  cvmcov  32510  cvmseu  32523  sat1el2xp  32626  hilbert1.2  33616  fneint  33696  elintabg  39954  mnuprdlem1  40628  mnuprdlem2  40629  mnuprdlem4  40631  elunif  41293  fnchoice  41306  lmbr3  42048