Theorem elequ2 2141

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 2139	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
2		ax-14 2139	. . 3 ⊢ (𝑦 = 𝑥 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥))
3	2	equcoms 1696	. 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 1437  ax-ie2 1482  ax-8 1492  ax-17 1514  ax-i9 1518  ax-14 2139

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  elsb2  2144  dveel2  2146  axext3  2148  axext4  2149  bm1.1  2150  eleq2w  2228  bm1.3ii  4103  nalset  4112  zfun  4412  fv3  5509  tfrlemisucaccv  6293  tfr1onlemsucaccv  6309  tfrcllemsucaccv  6322  acfun  7163  ccfunen  7205  cc1  7206  bdsepnft  13769  bdsepnfALT  13771  bdbm1.3ii  13773  bj-nalset  13777  bj-nnelirr  13835  nninfalllem1  13888  nninfsellemeq  13894  nninfsellemqall  13895  nninfsellemeqinf  13896  nninfomni  13899