Theorem elequ2 1649

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 1451	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
2		ax-14 1451	. . 3 ⊢ (𝑦 = 𝑥 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥))
3	2	equcoms 1642	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥))
4	1, 3	impbid 128	1 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1384  ax-ie2 1429  ax-8 1441  ax-14 1451  ax-17 1465  ax-i9 1469

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  elsb4  1902  dveel2  1946  axext3  2072  axext4  2073  bm1.1  2074  eleq2w  2150  bm1.3ii  3966  nalset  3975  zfun  4270  fv3  5341  tfrlemisucaccv  6104  tfr1onlemsucaccv  6120  tfrcllemsucaccv  6133  bdsepnft  12044  bdsepnfALT  12046  bdbm1.3ii  12048  bj-nalset  12052  bj-nnelirr  12114  strcollnft  12145  strcollnfALT  12147  nninfalllem1  12165  nninfsellemeq  12172  nninfsellemqall  12173  nninfsellemeqinf  12174  nninfomni  12177