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  4872  elintabg  4908  cantnflem1c  9583  tcrank  9783  isf32lem2  10251  sadcp1  16372  subgacs  19079  nsgacs  19080  sdrgacs  20722  lssacs  20906  elcls3  23004  conncompconn  23353  1stcfb  23366  dfac14lem  23538  r0cld  23659  uffix  23842  flftg  23917  tgpconncompeqg  24033  wilth  27014  tghilberti2  28622  umgr2edgneu  29199  uspgredg2v  29209  usgredgleordALT  29219  nbusgrf1o  29356  vtxdushgrfvedglem  29475  constrmon  33764  ddemeas  34256  cvmcov  35314  cvmseu  35327  sat1el2xp  35430  hilbert1.2  36206  fneint  36399  mnuprdlem1  44370  mnuprdlem2  44371  mnuprdlem4  44373  elunif  45118  fnchoice  45131  lmbr3  45850