Theorem vtoclbg 3514

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

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

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 2115

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

This theorem is referenced by:  alexeqg  3605  pm13.183  3620  elab6g  3623  elabgw  3632  sbc8g  3748  sbc2or  3749  sbccow  3763  sbcco  3766  sbc5ALT  3769  sbcie2g  3781  eqsbc1  3787  sbcng  3788  sbcimg  3789  sbcan  3790  sbcor  3791  sbcbig  3792  sbcal  3800  sbcex2  3801  sbcel1v  3806  sbcreu  3826  csbiebg  3881  sbcel12  4363  sbceqg  4364  csbie2df  4395  preq12bg  4809  elintrabg  4916  sbcbr123  5152  inisegn0  6057  fsn2g  7083  funfvima3  7182  elixpsn  8875  ixpsnf1o  8876  domeng  8899  rankcf  10688  eldm3  35955  elima4  35970  brsset  36081  brbigcup  36090  elfix2  36096  elfunsg  36108  elsingles  36110  funpartlem  36136  ellines  36346  elhf2g  36370  bj-elpwgALT  37255  cover2g  37917  sbcrexgOLD  43037