Theorem elequ2 2214

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1502  ax-ie2 1547  ax-8 1557  ax-17 1579  ax-i9 1583  ax-14 2212

This proof depends on definitions:  df-bi 117

This theorem is used by:  elsb2  2217  dveel2  2219  axext3  2221  axext4  2222  bm1.1  2223  eleq2w  2300  bm1.3ii  4254  nalset  4263  zfun  4579  fv3  5718  tfrlemisucaccv  6596  tfr1onlemsucaccv  6612  tfrcllemsucaccv  6625  sspw1or2  7545  acfun  7564  ccfunen  7631  cc1  7632  nninfinf  10895  bdsepnft  17079  bdsepnfALT  17081  bdbm1.3ii  17083  bj-nalset  17087  bj-nnelirr  17145  nninfalllem1  17217  nninfsellemeq  17223  nninfsellemqall  17224  nninfsellemeqinf  17225  nninfomni  17228