Theorem ensymd 6740

Description: Symmetry of equinumerosity. Deduction form of ensym 6738. (Contributed by David Moews, 1-May-2017.)

Hypothesis

Ref	Expression
ensymd.1	⊢ (𝜑 → 𝐴 ≈ 𝐵)

Assertion

Ref	Expression
ensymd	⊢ (𝜑 → 𝐵 ≈ 𝐴)

Proof of Theorem ensymd

Step	Hyp	Ref	Expression
1		ensymd.1	. 2 ⊢ (𝜑 → 𝐴 ≈ 𝐵)
2		ensym 6738	. 2 ⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴)
3	1, 2	syl 14	1 ⊢ (𝜑 → 𝐵 ≈ 𝐴)

Syntax hints:   → wi 4   class class class wbr 3976   ≈ cen 6695

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-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-13 2137  ax-14 2138  ax-ext 2146  ax-sep 4094  ax-pow 4147  ax-pr 4181  ax-un 4405

This theorem depends on definitions:  df-bi 116  df-3an 969  df-tru 1345  df-nf 1448  df-sb 1750  df-eu 2016  df-mo 2017  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-ral 2447  df-rex 2448  df-v 2723  df-un 3115  df-in 3117  df-ss 3124  df-pw 3555  df-sn 3576  df-pr 3577  df-op 3579  df-uni 3784  df-br 3977  df-opab 4038  df-id 4265  df-xp 4604  df-rel 4605  df-cnv 4606  df-co 4607  df-dm 4608  df-rn 4609  df-res 4610  df-ima 4611  df-fun 5184  df-fn 5185  df-f 5186  df-f1 5187  df-fo 5188  df-f1o 5189  df-er 6492  df-en 6698

This theorem is referenced by:  f1imaeng  6749  f1imaen2g  6750  en2sn  6770  xpdom3m  6791  phplem4  6812  phplem4dom  6819  php5dom  6820  phpm  6822  phplem4on  6824  dif1en  6836  dif1enen  6837  fisbth  6840  fin0  6842  fin0or  6843  fientri3  6871  unsnfidcex  6876  unsnfidcel  6877  fiintim  6885  fisseneq  6888  f1ofi  6899  endjusym  7052  eninl  7053  eninr  7054  pm54.43  7137  djuen  7158  dju1en  7160  djuassen  7164  xpdjuen  7165  uzenom  10350  hashennnuni  10681  hashennn  10682  hashcl  10683  hashfz1  10685  hashen  10686  fihashfn  10702  fihashdom  10705  hashunlem  10706  zfz1iso  10740  summodclem2  11309  zsumdc  11311  prodmodclem2  11504  zproddc  11506  ennnfonelemen  12291  exmidunben  12296  ctinfom  12298  ctinf  12300  pwf1oexmid  13713  sbthom  13739