Theorem eleq2w 2821

Description: Weaker version of eleq2 2826 (but more general than elequ2 2129) not depending on ax-ext 2709 nor df-cleq 2729. (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 631	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ (𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦)))
3	2	exbidv 1923	. 2 ⊢ (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦)))
4		dfclel 2813	. 2 ⊢ (𝐴 ∈ 𝑥 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥))
5		dfclel 2813	. 2 ⊢ (𝐴 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦))
6	3, 4, 5	3bitr4g 314	1 ⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-clel 2812

This theorem is referenced by:  clelsb2  2865  eluniab  4878  elintabg  4914  cantnflem1c  9600  tcrank  9800  isf32lem2  10268  sadcp1  16386  subgacs  19094  nsgacs  19095  sdrgacs  20738  lssacs  20922  elcls3  23031  conncompconn  23380  1stcfb  23393  dfac14lem  23565  r0cld  23686  uffix  23869  flftg  23944  tgpconncompeqg  24060  wilth  27041  tghilberti2  28714  umgr2edgneu  29291  uspgredg2v  29301  usgredgleordALT  29311  nbusgrf1o  29448  vtxdushgrfvedglem  29567  constrmon  33903  ddemeas  34395  cvmcov  35459  cvmseu  35472  sat1el2xp  35575  hilbert1.2  36351  fneint  36544  mnuprdlem1  44580  mnuprdlem2  44581  mnuprdlem4  44583  elunif  45328  fnchoice  45341  lmbr3  46058