Theorem eleq2w 2862

Description: Weaker version of eleq2 2867 (but more general than elequ2 2171) not depending on ax-ext 2777 nor df-cleq 2792. (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 2171	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))
2	1	anbi2d 623	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ (𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦)))
3	2	exbidv 2017	. 2 ⊢ (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥) ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦)))
4		df-clel 2795	. 2 ⊢ (𝐴 ∈ 𝑥 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥))
5		df-clel 2795	. 2 ⊢ (𝐴 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦))
6	3, 4, 5	3bitr4g 306	1 ⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 385   = wceq 1653  ∃wex 1875   ∈ wcel 2157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166

This theorem depends on definitions:  df-bi 199  df-an 386  df-ex 1876  df-clel 2795

This theorem is referenced by:  eluniab  4639  elintab  4678  cantnflem1c  8834  tcrank  8997  isf32lem2  9464  sadcp1  15512  subgacs  17942  nsgacs  17943  lssacs  19288  elcls3  21216  conncompconn  21564  1stcfb  21577  dfac14lem  21749  r0cld  21870  uffix  22053  flftg  22128  tgpconncompeqg  22243  wilth  25149  tghilberti2  25889  umgr2edgneu  26447  uspgredg2v  26457  usgredgleordALT  26468  nbusgrf1o  26615  vtxdushgrfvedglem  26739  ddemeas  30815  cvmcov  31762  cvmseu  31775  hilbert1.2  32775  fneint  32855  sdrgacs  38556  elintabg  38663  elunif  39935  fnchoice  39948  lmbr3  40723