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  15756  bdsepnfALT  15758  bdbm1.3ii  15760  bj-nalset  15764  bj-nnelirr  15822  nninfalllem1  15878  nninfsellemeq  15884  nninfsellemqall  15885  nninfsellemeqinf  15886  nninfomni  15889