Theorem riota2 7134

Description: This theorem shows a condition that allows us to represent a descriptor with a class expression 𝐵. (Contributed by NM, 23-Aug-2011.) (Revised by Mario Carneiro, 10-Dec-2016.)

Hypothesis

Ref	Expression
riota2.1	⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
riota2	⊢ ((𝐵 ∈ 𝐴 ∧ ∃!𝑥 ∈ 𝐴 𝜑) → (𝜓 ↔ (℩𝑥 ∈ 𝐴 𝜑) = 𝐵))

Distinct variable groups:   𝜓,𝑥   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem riota2

Step	Hyp	Ref	Expression
1		nfcv 2920	. 2 ⊢ Ⅎ𝑥𝐵
2		nfv 1916	. 2 ⊢ Ⅎ𝑥𝜓
3		riota2.1	. 2 ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓))
4	1, 2, 3	riota2f 7133	1 ⊢ ((𝐵 ∈ 𝐴 ∧ ∃!𝑥 ∈ 𝐴 𝜑) → (𝜓 ↔ (℩𝑥 ∈ 𝐴 𝜑) = 𝐵))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1539   ∈ wcel 2112  ∃!wreu 3073  ℩crio 7108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3an 1087  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ral 3076  df-rex 3077  df-reu 3078  df-v 3412  df-sbc 3698  df-un 3864  df-in 3866  df-ss 3876  df-sn 4524  df-pr 4526  df-uni 4800  df-iota 6295  df-riota 7109

This theorem is referenced by:  eqsup  8954  sup0  8964  fin23lem22  9788  subadd  10928  divmul  11340  fllelt  13217  flflp1  13227  flval2  13234  flbi  13236  remim  14525  resqrtcl  14662  resqrtthlem  14663  sqrtneg  14676  sqrtthlem  14771  divalgmod  15808  qnumdenbi  16140  catidd  17010  lubprop  17663  glbprop  17676  isglbd  17794  poslubd  17825  ismgmid  17942  isgrpinv  18224  pj1id  18893  coeeq  24924  ismir  26553  mireq  26559  ismidb  26672  islmib  26681  usgredg2vlem2  27116  frgrncvvdeqlem3  28186  frgr2wwlkeqm  28216  cnidOLD  28465  hilid  29044  pjpreeq  29281  cnvbraval  29993  cdj3lem2  30318  xdivmul  30724  cvmliftphtlem  32796  cvmlift3lem4  32801  cvmlift3lem6  32803  cvmlift3lem9  32806  scutbday  33560  eqscut  33561  scutun12  33566  scutbdaylt  33574  transportprops  33886  ltflcei  35326  cmpidelt  35578  exidresid  35598  lshpkrlem1  36687  cdlemeiota  38162  dochfl1  39053  hgmapvs  39468  evlsval3  39778  fsuppind  39785  renegadd  39853  resubadd  39860  addinvcom  39911  wessf1ornlem  42182  fourierdlem50  43165