Theorem eleq2w 2815

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541  ∃wex 1780   ∈ wcel 2111

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-8 2113  ax-9 2121

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

This theorem is referenced by:  clelsb2  2859  eluniab  4870  elintabg  4906  cantnflem1c  9577  tcrank  9777  isf32lem2  10245  sadcp1  16366  subgacs  19073  nsgacs  19074  sdrgacs  20716  lssacs  20900  elcls3  22998  conncompconn  23347  1stcfb  23360  dfac14lem  23532  r0cld  23653  uffix  23836  flftg  23911  tgpconncompeqg  24027  wilth  27008  tghilberti2  28616  umgr2edgneu  29192  uspgredg2v  29202  usgredgleordALT  29212  nbusgrf1o  29349  vtxdushgrfvedglem  29468  constrmon  33757  ddemeas  34249  cvmcov  35307  cvmseu  35320  sat1el2xp  35423  hilbert1.2  36199  fneint  36392  mnuprdlem1  44364  mnuprdlem2  44365  mnuprdlem4  44367  elunif  45112  fnchoice  45125  lmbr3  45844