Theorem riota2 6777

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 382   = wceq 1631   ∈ wcel 2145  ∃!wreu 3063  ℩crio 6754

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-reu 3068  df-v 3353  df-sbc 3589  df-un 3729  df-sn 4318  df-pr 4320  df-uni 4576  df-iota 5995  df-riota 6755

This theorem is referenced by:  eqsup  8519  sup0  8529  fin23lem22  9352  subadd  10487  divmul  10891  fllelt  12807  flflp1  12817  flval2  12824  flbi  12826  remim  14066  resqrtcl  14203  resqrtthlem  14204  sqrtneg  14217  sqrtthlem  14311  divalgmod  15338  divalgmodOLD  15339  qnumdenbi  15660  catidd  16549  lubprop  17195  glbprop  17208  isglbd  17326  poslubd  17357  ismgmid  17473  isgrpinv  17681  pj1id  18320  coeeq  24204  ismir  25776  mireq  25782  ismidb  25892  islmib  25901  usgredg2vlem2  26341  frgrncvvdeqlem3  27484  frgr2wwlkeqm  27514  cnidOLD  27778  hilid  28359  pjpreeq  28598  cnvbraval  29310  cdj3lem2  29635  xdivmul  29974  cvmliftphtlem  31638  cvmlift3lem4  31643  cvmlift3lem6  31645  cvmlift3lem9  31648  scutbday  32251  scutun12  32255  scutbdaylt  32260  transportprops  32479  ltflcei  33731  cmpidelt  33991  exidresid  34011  lshpkrlem1  34920  cdlemeiota  36395  dochfl1  37287  hgmapvs  37702  wessf1ornlem  39892  fourierdlem50  40891