Theorem riota2 7369

Description: This theorem shows a condition that allows 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 2891	. 2 ⊢ Ⅎ𝑥𝐵
2		nfv 1914	. 2 ⊢ Ⅎ𝑥𝜓
3		riota2.1	. 2 ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓))
4	1, 2, 3	riota2f 7368	1 ⊢ ((𝐵 ∈ 𝐴 ∧ ∃!𝑥 ∈ 𝐴 𝜑) → (𝜓 ↔ (℩𝑥 ∈ 𝐴 𝜑) = 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∃!wreu 3352  ℩crio 7343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-reu 3355  df-v 3449  df-un 3919  df-ss 3931  df-sn 4590  df-pr 4592  df-uni 4872  df-iota 6464  df-riota 7344

This theorem is referenced by:  eqsup  9407  sup0  9418  ttrcltr  9669  fin23lem22  10280  subadd  11424  divmul  11840  fllelt  13759  flflp1  13769  flval2  13776  flbi  13778  remim  15083  resqrtcl  15219  resqrtthlem  15220  sqrtneg  15233  sqrtthlem  15329  divalgmod  16376  qnumdenbi  16714  catidd  17641  lubprop  18317  glbprop  18330  poslubd  18372  isglbd  18468  ismgmid  18592  isgrpinv  18925  pj1id  19629  coeeq  26132  scutbday  27716  eqscut  27717  scutun12  27722  scutbdaylt  27730  divsmulw  28096  ismir  28586  mireq  28592  ismidb  28705  islmib  28714  usgredg2vlem2  29153  frgrncvvdeqlem3  30230  frgr2wwlkeqm  30260  cnidOLD  30511  hilid  31090  pjpreeq  31327  cnvbraval  32039  cdj3lem2  32364  xdivmul  32845  cvmliftphtlem  35304  cvmlift3lem4  35309  cvmlift3lem6  35311  cvmlift3lem9  35314  transportprops  36022  ltflcei  37602  cmpidelt  37853  exidresid  37873  lshpkrlem1  39103  cdlemeiota  40579  dochfl1  41470  hgmapvs  41885  renegadd  42360  resubadd  42367  addinvcom  42420  redivmuld  42433  evlsval3  42547  fsuppind  42578  wessf1ornlem  45179  fourierdlem50  46154