Theorem elequ2 2207

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 2205	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
2		ax-14 2205	. . 3 ⊢ (𝑦 = 𝑥 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥))
3	2	equcoms 1756	. 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 1497  ax-ie2 1542  ax-8 1552  ax-17 1574  ax-i9 1578  ax-14 2205

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  elsb2  2210  dveel2  2212  axext3  2214  axext4  2215  bm1.1  2216  eleq2w  2293  bm1.3ii  4210  nalset  4219  zfun  4531  fv3  5662  tfrlemisucaccv  6491  tfr1onlemsucaccv  6507  tfrcllemsucaccv  6520  sspw1or2  7403  acfun  7422  ccfunen  7483  cc1  7484  nninfinf  10706  bdsepnft  16508  bdsepnfALT  16510  bdbm1.3ii  16512  bj-nalset  16516  bj-nnelirr  16574  nninfalllem1  16636  nninfsellemeq  16642  nninfsellemqall  16643  nninfsellemeqinf  16644  nninfomni  16647