Theorem vtoclbg 3559

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 345	. 2 ⊢ (𝑥 = 𝐴 → ((𝜑 ↔ 𝜓) ↔ (𝜒 ↔ 𝜃)))
4		vtoclbg.3	. 2 ⊢ (𝜑 ↔ 𝜓)
5	3, 4	vtoclg 3556	1 ⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ∈ wcel 2106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-clel 2810

This theorem is referenced by:  alexeqg  3639  pm13.183  3656  elab6g  3659  sbc8g  3785  sbc2or  3786  sbccow  3800  sbcco  3803  sbc5ALT  3806  sbcie2g  3819  eqsbc1  3826  sbcng  3827  sbcimg  3828  sbcan  3829  sbcor  3830  sbcbig  3831  sbcal  3841  sbcex2  3842  sbcel1v  3848  sbcreu  3870  csbiebg  3926  sbcel12  4408  sbceqg  4409  csbie2df  4440  preq12bg  4854  elintrabg  4965  sbcbr123  5202  inisegn0  6097  fsn2g  7138  funfvima3  7240  elixpsn  8933  ixpsnf1o  8934  domeng  8960  1sdomOLD  9251  rankcf  10774  eldm3  35023  elima4  35039  brsset  35153  brbigcup  35162  elfix2  35168  elfunsg  35180  elsingles  35182  funpartlem  35206  ellines  35416  elhf2g  35440  bj-elpwgALT  36238  cover2g  36887  elabgw  41710  sbcrexgOLD  41825