Theorem ralsng 4409

Description: Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2015.)

Hypothesis

Ref	Expression
ralsng.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
ralsng	⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓))

Distinct variable groups:   𝑥,𝐴   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝑉(𝑥)

Proof of Theorem ralsng

Step	Hyp	Ref	Expression
1		ralsnsg 4407	. 2 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ [𝐴 / 𝑥]𝜑))
2		ralsng.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	2	sbcieg 3666	. 2 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜓))
4	1, 3	bitrd 271	1 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1653   ∈ wcel 2157  ∀wral 3089  [wsbc 3633  {csn 4368

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2777

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-ral 3094  df-v 3387  df-sbc 3634  df-sn 4369

This theorem is referenced by:  2ralsng  4411  ralsn  4413  ralprg  4424  raltpg  4426  ralunsn  4614  iinxsng  4790  frirr  5289  posn  5392  frsn  5394  f12dfv  6757  ranksnb  8940  mgm1  17572  sgrp1  17608  mnd1  17646  grp1  17838  cntzsnval  18069  abl1  18584  srgbinomlem4  18859  ring1  18918  mat1dimmul  20608  ufileu  22051  istrkg3ld  25712  1hevtxdg0  26755  wlkp1lem8  26933  wwlksnext  27162  wwlksext2clwwlk  27373  wwlksext2clwwlkOLD  27374  dfconngr1  27532  1conngr  27538  frgr1v  27620  poimirlem26  33924  poimirlem27  33925  poimirlem31  33929  zlidlring  42727  linds0  43053  snlindsntor  43059  lmod1  43080