Theorem vtoclbg 3512

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 29-Apr-1994.)

Hypotheses

Ref	Expression
vtoclbg.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
vtoclbg.2	⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))
vtoclbg.3	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
vtoclbg	⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃))

Distinct variable groups:   𝑥,𝐴   𝜒,𝑥   𝜃,𝑥

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

Proof of Theorem vtoclbg

Step	Hyp	Ref	Expression
1		vtoclbg.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
2		vtoclbg.2	. . 3 ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))
3	1, 2	bibi12d 346	. 2 ⊢ (𝑥 = 𝐴 → ((𝜑 ↔ 𝜓) ↔ (𝜒 ↔ 𝜃)))
4		vtoclbg.3	. 2 ⊢ (𝜑 ↔ 𝜓)
5	3, 4	vtoclg 3510	1 ⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2714  df-clel 2814

This theorem is referenced by:  alexeqg  3586  pm13.183  3602  elab6g  3605  sbc8g  3729  sbc2or  3730  sbccow  3744  sbcco  3747  sbc5ALT  3750  sbcie2g  3763  eqsbc1  3770  sbcng  3771  sbcimg  3772  sbcan  3773  sbcor  3774  sbcbig  3775  sbcal  3785  sbcex2  3786  sbcel1v  3792  sbcreu  3814  csbiebg  3870  sbcel12  4348  sbceqg  4349  csbie2df  4380  preq12bg  4790  elintrabg  4899  sbcbr123  5135  inisegn0  6016  fsn2g  7042  funfvima3  7144  elixpsn  8756  ixpsnf1o  8757  domeng  8783  1sdomOLD  9070  rankcf  10579  eldm3  33773  elima4  33795  brsset  34236  brbigcup  34245  elfix2  34251  elfunsg  34263  elsingles  34265  funpartlem  34289  ellines  34499  elhf2g  34523  cover2g  35917  elabgw  40207  sbcrexgOLD  40644