Theorem eleq2w 2848

Description: Weaker version of eleq2 2853 (but more general than elequ2 2159) not depending on ax-ext 2736 nor df-cleq 2756. (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 2159	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))
2	1	anbi2d 639	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ (𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦)))
3	2	exbidv 1943	. 2 ⊢ (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦)))
4		dfclel 2840	. 2 ⊢ (𝐴 ∈ 𝑥 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥))
5		dfclel 2840	. 2 ⊢ (𝐴 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦))
6	3, 4, 5	3bitr4g 316	1 ⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1562  ∃wex 1801   ∈ wcel 2144

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802  df-clel 2839

This theorem is referenced by:  clelsb2  2892  eluniab  4881  elintabg  4918  cantnflem1c  9644  tcrank  9844  isf32lem2  10313  sadcp1  16491  subgacs  19204  nsgacs  19205  sdrgacs  20852  lssacs  21036  elcls3  23145  conncompconn  23494  1stcfb  23507  dfac14lem  23679  r0cld  23800  uffix  23983  flftg  24058  tgpconncompeqg  24174  wilth  27137  tghilberti2  28809  umgr2edgneu  29417  uspgredg2v  29427  usgredgleordALT  29437  nbusgrf1o  29574  vtxdushgrfvedglem  29692  constrmon  34043  ddemeas  34535  cvmcov  35618  cvmseu  35631  sat1el2xp  35734  hilbert1.2  36510  fneint  36713  mnuprdlem1  44853  mnuprdlem2  44854  mnuprdlem4  44856  elunif  45601  fnchoice  45614  lmbr3  46326