Theorem ensymd 6962

Description: Symmetry of equinumerosity. Deduction form of ensym 6960. (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 6960	. 2 ⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴)
3	1, 2	syl 14	1 ⊢ (𝜑 → 𝐵 ≈ 𝐴)

Syntax hints:   → wi 4   class class class wbr 4089   ≈ cen 6912

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-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2203  ax-14 2204  ax-ext 2212  ax-sep 4208  ax-pow 4266  ax-pr 4301  ax-un 4532

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1810  df-eu 2081  df-mo 2082  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-ral 2514  df-rex 2515  df-v 2803  df-un 3203  df-in 3205  df-ss 3212  df-pw 3655  df-sn 3676  df-pr 3677  df-op 3679  df-uni 3895  df-br 4090  df-opab 4152  df-id 4392  df-xp 4733  df-rel 4734  df-cnv 4735  df-co 4736  df-dm 4737  df-rn 4738  df-res 4739  df-ima 4740  df-fun 5330  df-fn 5331  df-f 5332  df-f1 5333  df-fo 5334  df-f1o 5335  df-er 6707  df-en 6915

This theorem is referenced by:  f1imaeng  6971  f1imaen2g  6972  en2sn  6993  xpdom3m  7023  phplem4  7046  phplem4dom  7053  php5dom  7054  phpm  7057  phplem4on  7059  dif1en  7073  dif1enen  7074  fisbth  7077  fin0  7079  fin0or  7080  fidcen  7093  fientri3  7112  unsnfidcex  7117  unsnfidcel  7118  fiintim  7128  fisseneq  7132  f1ofi  7147  endjusym  7300  eninl  7301  eninr  7302  pm54.43  7400  djuen  7431  dju1en  7433  djuassen  7437  xpdjuen  7438  uzenom  10693  hashennnuni  11047  hashennn  11048  hashcl  11049  hashfz1  11051  hashen  11052  fihashfn  11069  fihashdom  11072  hashunlem  11073  zfz1iso  11111  summodclem2  11966  zsumdc  11968  prodmodclem2  12161  zproddc  12163  4sqlem11  12997  ennnfonelemen  13065  exmidunben  13070  ctinfom  13072  ctinf  13074  isnzr2  14222  znfi  14693  znhash  14694  usgrsizedgen  16093  upgr2wlkdc  16257  eupthfi  16331  pwf1oexmid  16660  nnnninfen  16686  sbthom  16693