Theorem eleq2w 2812

Description: Weaker version of eleq2 2817 (but more general than elequ2 2124) not depending on ax-ext 2701 nor df-cleq 2721. (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 2124	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))
2	1	anbi2d 630	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ (𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦)))
3	2	exbidv 1921	. 2 ⊢ (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦)))
4		dfclel 2804	. 2 ⊢ (𝐴 ∈ 𝑥 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥))
5		dfclel 2804	. 2 ⊢ (𝐴 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦))
6	3, 4, 5	3bitr4g 314	1 ⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2803

This theorem is referenced by:  clelsb2  2856  eluniab  4872  elintabg  4907  elintabOLD  4909  cantnflem1c  9583  tcrank  9780  isf32lem2  10248  sadcp1  16366  subgacs  19040  nsgacs  19041  sdrgacs  20686  lssacs  20870  elcls3  22968  conncompconn  23317  1stcfb  23330  dfac14lem  23502  r0cld  23623  uffix  23806  flftg  23881  tgpconncompeqg  23997  wilth  26979  tghilberti2  28587  umgr2edgneu  29163  uspgredg2v  29173  usgredgleordALT  29183  nbusgrf1o  29320  vtxdushgrfvedglem  29439  constrmon  33727  ddemeas  34219  cvmcov  35256  cvmseu  35269  sat1el2xp  35372  hilbert1.2  36149  fneint  36342  mnuprdlem1  44265  mnuprdlem2  44266  mnuprdlem4  44268  elunif  45014  fnchoice  45027  lmbr3  45748