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 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))

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 1502  ax-ie2 1547  ax-8 1557  ax-17 1579  ax-i9 1583  ax-14 2212

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  elsb2  2217  dveel2  2219  axext3  2221  axext4  2222  bm1.1  2223  eleq2w  2300  bm1.3ii  4249  nalset  4258  zfun  4574  fv3  5713  tfrlemisucaccv  6586  tfr1onlemsucaccv  6602  tfrcllemsucaccv  6615  sspw1or2  7534  acfun  7553  ccfunen  7620  cc1  7621  nninfinf  10858  bdsepnft  16827  bdsepnfALT  16829  bdbm1.3ii  16831  bj-nalset  16835  bj-nnelirr  16893  nninfalllem1  16956  nninfsellemeq  16962  nninfsellemqall  16963  nninfsellemeqinf  16964  nninfomni  16967