Theorem elequ2 2182

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 2180	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
2		ax-14 2180	. . 3 ⊢ (𝑦 = 𝑥 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥))
3	2	equcoms 1732	. 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 1473  ax-ie2 1518  ax-8 1528  ax-17 1550  ax-i9 1554  ax-14 2180

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  elsb2  2185  dveel2  2187  axext3  2189  axext4  2190  bm1.1  2191  eleq2w  2268  bm1.3ii  4173  nalset  4182  zfun  4489  fv3  5612  tfrlemisucaccv  6424  tfr1onlemsucaccv  6440  tfrcllemsucaccv  6453  acfun  7335  ccfunen  7396  cc1  7397  nninfinf  10610  bdsepnft  15961  bdsepnfALT  15963  bdbm1.3ii  15965  bj-nalset  15969  bj-nnelirr  16027  nninfalllem1  16086  nninfsellemeq  16092  nninfsellemqall  16093  nninfsellemeqinf  16094  nninfomni  16097