Theorem riota2 6990

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 2947	. 2 ⊢ Ⅎ𝑥𝐵
2		nfv 1890	. 2 ⊢ Ⅎ𝑥𝜓
3		riota2.1	. 2 ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓))
4	1, 2, 3	riota2f 6989	1 ⊢ ((𝐵 ∈ 𝐴 ∧ ∃!𝑥 ∈ 𝐴 𝜑) → (𝜓 ↔ (℩𝑥 ∈ 𝐴 𝜑) = 𝐵))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1520   ∈ wcel 2079  ∃!wreu 3105  ℩crio 6967

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-13 2342  ax-ext 2767

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1080  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-mo 2574  df-eu 2610  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-ral 3108  df-rex 3109  df-reu 3110  df-v 3434  df-sbc 3702  df-un 3859  df-sn 4467  df-pr 4469  df-uni 4740  df-iota 6181  df-riota 6968

This theorem is referenced by:  eqsup  8756  sup0  8766  fin23lem22  9584  subadd  10725  divmul  11138  fllelt  13005  flflp1  13015  flval2  13022  flbi  13024  remim  14298  resqrtcl  14435  resqrtthlem  14436  sqrtneg  14449  sqrtthlem  14544  divalgmod  15578  qnumdenbi  15901  catidd  16768  lubprop  17413  glbprop  17426  isglbd  17544  poslubd  17575  ismgmid  17691  isgrpinv  17901  pj1id  18540  coeeq  24488  ismir  26115  mireq  26121  ismidb  26234  islmib  26243  usgredg2vlem2  26679  frgrncvvdeqlem3  27760  frgr2wwlkeqm  27790  cnidOLD  28038  hilid  28617  pjpreeq  28854  cnvbraval  29566  cdj3lem2  29891  xdivmul  30256  cvmliftphtlem  32128  cvmlift3lem4  32133  cvmlift3lem6  32135  cvmlift3lem9  32138  scutbday  32821  scutun12  32825  scutbdaylt  32830  transportprops  33049  ltflcei  34357  cmpidelt  34615  exidresid  34635  lshpkrlem1  35727  cdlemeiota  37202  dochfl1  38093  hgmapvs  38508  renegadd  38674  resubadd  38682  wessf1ornlem  40938  fourierdlem50  41937