Theorem elequ2 2205

Description: An identity law for the non-logical predicate. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
elequ2	⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))

Proof of Theorem elequ2

Step	Hyp	Ref	Expression
1		ax-14 2203	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
2		ax-14 2203	. . 3 ⊢ (𝑦 = 𝑥 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥))
3	2	equcoms 1754	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥))
4	1, 3	impbid 129	1 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1495  ax-ie2 1540  ax-8 1550  ax-17 1572  ax-i9 1576  ax-14 2203

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  elsb2  2208  dveel2  2210  axext3  2212  axext4  2213  bm1.1  2214  eleq2w  2291  bm1.3ii  4205  nalset  4214  zfun  4525  fv3  5652  tfrlemisucaccv  6477  tfr1onlemsucaccv  6493  tfrcllemsucaccv  6506  acfun  7400  ccfunen  7461  cc1  7462  nninfinf  10677  bdsepnft  16305  bdsepnfALT  16307  bdbm1.3ii  16309  bj-nalset  16313  bj-nnelirr  16371  nninfalllem1  16434  nninfsellemeq  16440  nninfsellemqall  16441  nninfsellemeqinf  16442  nninfomni  16445