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  6490  tfr1onlemsucaccv  6506  tfrcllemsucaccv  6519  sspw1or2  7402  acfun  7421  ccfunen  7482  cc1  7483  nninfinf  10704  bdsepnft  16482  bdsepnfALT  16484  bdbm1.3ii  16486  bj-nalset  16490  bj-nnelirr  16548  nninfalllem1  16610  nninfsellemeq  16616  nninfsellemqall  16617  nninfsellemeqinf  16618  nninfomni  16621