MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ralsng Structured version   Visualization version   GIF version

Theorem ralsng 4674
Description: Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2015.) Avoid ax-10 2140, ax-12 2176. (Revised by GG, 30-Sep-2024.)
Hypothesis
Ref Expression
ralsng.1 (𝑥 = 𝐴 → (𝜑𝜓))
Assertion
Ref Expression
ralsng (𝐴𝑉 → (∀𝑥 ∈ {𝐴}𝜑𝜓))
Distinct variable groups:   𝑥,𝐴   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝑉(𝑥)

Proof of Theorem ralsng
StepHypRef Expression
1 df-ral 3061 . . 3 (∀𝑥 ∈ {𝐴}𝜑 ↔ ∀𝑥(𝑥 ∈ {𝐴} → 𝜑))
2 velsn 4641 . . . . 5 (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
32imbi1i 349 . . . 4 ((𝑥 ∈ {𝐴} → 𝜑) ↔ (𝑥 = 𝐴𝜑))
43albii 1818 . . 3 (∀𝑥(𝑥 ∈ {𝐴} → 𝜑) ↔ ∀𝑥(𝑥 = 𝐴𝜑))
51, 4bitri 275 . 2 (∀𝑥 ∈ {𝐴}𝜑 ↔ ∀𝑥(𝑥 = 𝐴𝜑))
6 elisset 2822 . . 3 (𝐴𝑉 → ∃𝑥 𝑥 = 𝐴)
7 ralsng.1 . . . . . . 7 (𝑥 = 𝐴 → (𝜑𝜓))
87pm5.74i 271 . . . . . 6 ((𝑥 = 𝐴𝜑) ↔ (𝑥 = 𝐴𝜓))
98albii 1818 . . . . 5 (∀𝑥(𝑥 = 𝐴𝜑) ↔ ∀𝑥(𝑥 = 𝐴𝜓))
109a1i 11 . . . 4 (∃𝑥 𝑥 = 𝐴 → (∀𝑥(𝑥 = 𝐴𝜑) ↔ ∀𝑥(𝑥 = 𝐴𝜓)))
11 19.23v 1941 . . . . 5 (∀𝑥(𝑥 = 𝐴𝜓) ↔ (∃𝑥 𝑥 = 𝐴𝜓))
1211a1i 11 . . . 4 (∃𝑥 𝑥 = 𝐴 → (∀𝑥(𝑥 = 𝐴𝜓) ↔ (∃𝑥 𝑥 = 𝐴𝜓)))
13 pm5.5 361 . . . 4 (∃𝑥 𝑥 = 𝐴 → ((∃𝑥 𝑥 = 𝐴𝜓) ↔ 𝜓))
1410, 12, 133bitrd 305 . . 3 (∃𝑥 𝑥 = 𝐴 → (∀𝑥(𝑥 = 𝐴𝜑) ↔ 𝜓))
156, 14syl 17 . 2 (𝐴𝑉 → (∀𝑥(𝑥 = 𝐴𝜑) ↔ 𝜓))
165, 15bitrid 283 1 (𝐴𝑉 → (∀𝑥 ∈ {𝐴}𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wal 1537   = wceq 1539  wex 1778  wcel 2107  wral 3060  {csn 4625
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ral 3061  df-v 3481  df-sn 4626
This theorem is referenced by:  rexsng  4675  2ralsng  4677  ralsn  4680  ralprg  4695  raltpg  4697  ralunsn  4893  iinxsng  5087  frirr  5660  posn  5770  frsn  5772  f1ounsn  7293  f12dfv  7294  naddov2  8718  naddunif  8732  naddasslem1  8733  naddasslem2  8734  ranksnb  9868  mgm1  18672  sgrp1  18743  mnd1  18793  grp1  19066  cntzsnval  19343  abl1  19885  srgbinomlem4  20227  ring1  20308  mat1dimmul  22483  ufileu  23928  istrkg3ld  28470  1hevtxdg0  29524  wlkp1lem8  29699  wwlksnext  29914  wwlksext2clwwlk  30077  dfconngr1  30208  1conngr  30214  frgr1v  30291  lindssn  33407  lbslsat  33668  bj-raldifsn  37102  lindsadd  37621  poimirlem26  37654  poimirlem27  37655  poimirlem31  37659  cantnfresb  43342  safesnsupfilb  43436  cfsetsnfsetf1  47076  zlidlring  48155  linds0  48387  snlindsntor  48393  lmod1  48414
  Copyright terms: Public domain W3C validator