Theorem riota2 7344

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∃!wreu 3341  ℩crio 7318

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-reu 3344  df-v 3432  df-un 3895  df-ss 3907  df-sn 4569  df-pr 4571  df-uni 4852  df-iota 6450  df-riota 7319

This theorem is referenced by:  eqsup  9364  sup0  9375  ttrcltr  9632  fin23lem22  10244  subadd  11391  divmul  11807  fllelt  13751  flflp1  13761  flval2  13768  flbi  13770  remim  15074  resqrtcl  15210  resqrtthlem  15211  sqrtneg  15224  sqrtthlem  15320  divalgmod  16370  qnumdenbi  16709  catidd  17641  lubprop  18317  glbprop  18330  poslubd  18372  isglbd  18470  ismgmid  18628  isgrpinv  18964  pj1id  19669  evlsval3  22081  coeeq  26206  cutbday  27794  eqcuts  27795  cutsun12  27800  cutbdaylt  27808  divmulsw  28203  ismir  28745  mireq  28751  ismidb  28864  islmib  28873  usgredg2vlem2  29313  frgrncvvdeqlem3  30390  frgr2wwlkeqm  30420  cnidOLD  30672  hilid  31251  pjpreeq  31488  cnvbraval  32200  cdj3lem2  32525  xdivmul  33003  cvmliftphtlem  35519  cvmlift3lem4  35524  cvmlift3lem6  35526  cvmlift3lem9  35529  transportprops  36236  ltflcei  37949  cmpidelt  38200  exidresid  38220  lshpkrlem1  39576  cdlemeiota  41051  dochfl1  41942  hgmapvs  42357  renegadd  42824  resubadd  42831  addinvcom  42884  redivmuld  42897  fsuppind  43043  wessf1ornlem  45639  fourierdlem50  46608