Theorem elequ2 2180

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 2178	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
2		ax-14 2178	. . 3 ⊢ (𝑦 = 𝑥 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥))
3	2	equcoms 1730	. 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 1471  ax-ie2 1516  ax-8 1526  ax-17 1548  ax-i9 1552  ax-14 2178

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  elsb2  2183  dveel2  2185  axext3  2187  axext4  2188  bm1.1  2189  eleq2w  2266  bm1.3ii  4164  nalset  4173  zfun  4480  fv3  5598  tfrlemisucaccv  6410  tfr1onlemsucaccv  6426  tfrcllemsucaccv  6439  acfun  7318  ccfunen  7375  cc1  7376  nninfinf  10586  bdsepnft  15785  bdsepnfALT  15787  bdbm1.3ii  15789  bj-nalset  15793  bj-nnelirr  15851  nninfalllem1  15907  nninfsellemeq  15913  nninfsellemqall  15914  nninfsellemeqinf  15915  nninfomni  15918