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  4208  nalset  4217  zfun  4529  fv3  5658  tfrlemisucaccv  6486  tfr1onlemsucaccv  6502  tfrcllemsucaccv  6515  acfun  7412  ccfunen  7473  cc1  7474  nninfinf  10695  bdsepnft  16418  bdsepnfALT  16420  bdbm1.3ii  16422  bj-nalset  16426  bj-nnelirr  16484  nninfalllem1  16546  nninfsellemeq  16552  nninfsellemqall  16553  nninfsellemeqinf  16554  nninfomni  16557