Theorem elequ2 2210

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 2208	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
2		ax-14 2208	. . 3 ⊢ (𝑦 = 𝑥 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥))
3	2	equcoms 1756	. 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 1498  ax-ie2 1543  ax-8 1553  ax-17 1575  ax-i9 1579  ax-14 2208

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  elsb2  2213  dveel2  2215  axext3  2217  axext4  2218  bm1.1  2219  eleq2w  2296  bm1.3ii  4236  nalset  4245  zfun  4560  fv3  5698  tfrlemisucaccv  6569  tfr1onlemsucaccv  6585  tfrcllemsucaccv  6598  sspw1or2  7508  acfun  7527  ccfunen  7594  cc1  7595  nninfinf  10829  bdsepnft  16783  bdsepnfALT  16785  bdbm1.3ii  16787  bj-nalset  16791  bj-nnelirr  16849  nninfalllem1  16912  nninfsellemeq  16918  nninfsellemqall  16919  nninfsellemeqinf  16920  nninfomni  16923