Theorem vtoclbg 3510

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 3507	1 ⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-clel 2806

This theorem is referenced by:  alexeqg  3601  pm13.183  3616  elab6g  3619  elabgw  3628  sbc8g  3744  sbc2or  3745  sbccow  3759  sbcco  3762  sbc5ALT  3765  sbcie2g  3777  eqsbc1  3783  sbcng  3784  sbcimg  3785  sbcan  3786  sbcor  3787  sbcbig  3788  sbcal  3796  sbcex2  3797  sbcel1v  3802  sbcreu  3822  csbiebg  3877  sbcel12  4358  sbceqg  4359  csbie2df  4390  preq12bg  4802  elintrabg  4909  sbcbr123  5143  inisegn0  6046  fsn2g  7071  funfvima3  7170  elixpsn  8861  ixpsnf1o  8862  domeng  8885  rankcf  10668  eldm3  35805  elima4  35820  brsset  35931  brbigcup  35940  elfix2  35946  elfunsg  35958  elsingles  35960  funpartlem  35986  ellines  36196  elhf2g  36220  bj-elpwgALT  37098  cover2g  37766  sbcrexgOLD  42888