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

Theorem ralsng 4639
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 2138, ax-12 2172. (Revised by Gino Giotto, 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 3066 . . 3 (∀𝑥 ∈ {𝐴}𝜑 ↔ ∀𝑥(𝑥 ∈ {𝐴} → 𝜑))
2 velsn 4607 . . . . 5 (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
32imbi1i 350 . . . 4 ((𝑥 ∈ {𝐴} → 𝜑) ↔ (𝑥 = 𝐴𝜑))
43albii 1822 . . 3 (∀𝑥(𝑥 ∈ {𝐴} → 𝜑) ↔ ∀𝑥(𝑥 = 𝐴𝜑))
51, 4bitri 275 . 2 (∀𝑥 ∈ {𝐴}𝜑 ↔ ∀𝑥(𝑥 = 𝐴𝜑))
6 elisset 2820 . . 3 (𝐴𝑉 → ∃𝑥 𝑥 = 𝐴)
7 ralsng.1 . . . . . . 7 (𝑥 = 𝐴 → (𝜑𝜓))
87pm5.74i 271 . . . . . 6 ((𝑥 = 𝐴𝜑) ↔ (𝑥 = 𝐴𝜓))
98albii 1822 . . . . 5 (∀𝑥(𝑥 = 𝐴𝜑) ↔ ∀𝑥(𝑥 = 𝐴𝜓))
109a1i 11 . . . 4 (∃𝑥 𝑥 = 𝐴 → (∀𝑥(𝑥 = 𝐴𝜑) ↔ ∀𝑥(𝑥 = 𝐴𝜓)))
11 19.23v 1946 . . . . 5 (∀𝑥(𝑥 = 𝐴𝜓) ↔ (∃𝑥 𝑥 = 𝐴𝜓))
1211a1i 11 . . . 4 (∃𝑥 𝑥 = 𝐴 → (∀𝑥(𝑥 = 𝐴𝜓) ↔ (∃𝑥 𝑥 = 𝐴𝜓)))
13 pm5.5 362 . . . 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 205  wal 1540   = wceq 1542  wex 1782  wcel 2107  wral 3065  {csn 4591
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3066  df-v 3450  df-sn 4592
This theorem is referenced by:  rexsng  4640  2ralsng  4642  ralsn  4647  ralprg  4660  raltpg  4664  ralunsn  4856  iinxsng  5053  frirr  5615  posn  5722  frsn  5724  f12dfv  7224  naddov2  8630  naddunif  8644  naddasslem1  8645  naddasslem2  8646  ranksnb  9770  mgm1  18520  sgrp1  18562  mnd1  18604  grp1  18861  cntzsnval  19111  abl1  19651  srgbinomlem4  19967  ring1  20033  mat1dimmul  21841  ufileu  23286  istrkg3ld  27445  1hevtxdg0  28495  wlkp1lem8  28670  wwlksnext  28880  wwlksext2clwwlk  29043  dfconngr1  29174  1conngr  29180  frgr1v  29257  lindssn  32206  lbslsat  32353  bj-raldifsn  35600  lindsadd  36100  poimirlem26  36133  poimirlem27  36134  poimirlem31  36138  cantnfresb  41688  safesnsupfilb  41764  cfsetsnfsetf1  45367  zlidlring  46300  linds0  46620  snlindsntor  46626  lmod1  46647
  Copyright terms: Public domain W3C validator