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  4204  nalset  4213  zfun  4524  fv3  5649  tfrlemisucaccv  6469  tfr1onlemsucaccv  6485  tfrcllemsucaccv  6498  acfun  7385  ccfunen  7446  cc1  7447  nninfinf  10660  bdsepnft  16208  bdsepnfALT  16210  bdbm1.3ii  16212  bj-nalset  16216  bj-nnelirr  16274  nninfalllem1  16333  nninfsellemeq  16339  nninfsellemqall  16340  nninfsellemeqinf  16341  nninfomni  16344