Theorem ensymd 6882

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

Syntax hints:   → wi 4   class class class wbr 4047   ≈ cen 6832

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-13 2179  ax-14 2180  ax-ext 2188  ax-sep 4166  ax-pow 4222  ax-pr 4257  ax-un 4484

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-rex 2491  df-v 2775  df-un 3171  df-in 3173  df-ss 3180  df-pw 3619  df-sn 3640  df-pr 3641  df-op 3643  df-uni 3853  df-br 4048  df-opab 4110  df-id 4344  df-xp 4685  df-rel 4686  df-cnv 4687  df-co 4688  df-dm 4689  df-rn 4690  df-res 4691  df-ima 4692  df-fun 5278  df-fn 5279  df-f 5280  df-f1 5281  df-fo 5282  df-f1o 5283  df-er 6627  df-en 6835

This theorem is referenced by:  f1imaeng  6891  f1imaen2g  6892  en2sn  6912  xpdom3m  6936  phplem4  6959  phplem4dom  6966  php5dom  6967  phpm  6969  phplem4on  6971  dif1en  6983  dif1enen  6984  fisbth  6987  fin0  6989  fin0or  6990  fientri3  7019  unsnfidcex  7024  unsnfidcel  7025  fiintim  7035  fisseneq  7038  f1ofi  7052  endjusym  7205  eninl  7206  eninr  7207  pm54.43  7305  djuen  7330  dju1en  7332  djuassen  7336  xpdjuen  7337  uzenom  10577  hashennnuni  10931  hashennn  10932  hashcl  10933  hashfz1  10935  hashen  10936  fihashfn  10952  fihashdom  10955  hashunlem  10956  zfz1iso  10993  summodclem2  11737  zsumdc  11739  prodmodclem2  11932  zproddc  11934  4sqlem11  12768  ennnfonelemen  12836  exmidunben  12841  ctinfom  12843  ctinf  12845  isnzr2  13990  znfi  14461  znhash  14462  pwf1oexmid  16010  nnnninfen  16032  sbthom  16039