Theorem ralsng 4360

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 4358	. 2 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ [𝐴 / 𝑥]𝜑))
2		ralsng.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	2	sbcieg 3607	. 2 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜓))
4	1, 3	bitrd 268	1 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1630   ∈ wcel 2137  ∀wral 3048  [wsbc 3574  {csn 4319

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ral 3053  df-v 3340  df-sbc 3575  df-sn 4320

This theorem is referenced by:  2ralsng  4362  ralsn  4364  ralprg  4376  raltpg  4378  ralunsn  4572  iinxsng  4750  frirr  5241  posn  5342  frsn  5344  f12dfv  6690  ranksnb  8861  mgm1  17456  sgrp1  17492  mnd1  17530  grp1  17721  cntzsnval  17955  abl1  18467  srgbinomlem4  18741  ring1  18800  mat1dimmul  20482  ufileu  21922  istrkg3ld  25557  1hevtxdg0  26609  wlkp1lem8  26785  wwlksnext  27009  wwlksext2clwwlk  27185  wwlksext2clwwlkOLD  27186  dfconngr1  27338  1conngr  27344  frgr1v  27423  poimirlem26  33746  poimirlem27  33747  poimirlem31  33751  zlidlring  42436  linds0  42762  snlindsntor  42768  lmod1  42789