Theorem elequ2 2130

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

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1426  ax-ie2 1471  ax-8 1481  ax-17 1503  ax-i9 1507  ax-14 2128

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  elsb4  2133  dveel2  2135  axext3  2137  axext4  2138  bm1.1  2139  eleq2w  2216  bm1.3ii  4081  nalset  4090  zfun  4389  fv3  5484  tfrlemisucaccv  6262  tfr1onlemsucaccv  6278  tfrcllemsucaccv  6291  acfun  7121  ccfunen  7163  cc1  7164  bdsepnft  13400  bdsepnfALT  13402  bdbm1.3ii  13404  bj-nalset  13408  bj-nnelirr  13466  nninfalllem1  13521  nninfsellemeq  13527  nninfsellemqall  13528  nninfsellemeqinf  13529  nninfomni  13532