Theorem vtoclbg 3502

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114

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 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-clel 2811

This theorem is referenced by:  alexeqg  3593  pm13.183  3608  elab6g  3611  elabgw  3620  sbc8g  3736  sbc2or  3737  sbccow  3751  sbcco  3754  sbc5ALT  3757  sbcie2g  3769  eqsbc1  3775  sbcng  3776  sbcimg  3777  sbcan  3778  sbcor  3779  sbcbig  3780  sbcal  3788  sbcex2  3789  sbcel1v  3794  sbcreu  3814  csbiebg  3869  sbcel12  4351  sbceqg  4352  csbie2df  4383  preq12bg  4796  elintrabg  4903  sbcbr123  5139  inisegn0  6063  fsn2g  7091  funfvima3  7191  elixpsn  8885  ixpsnf1o  8886  domeng  8909  rankcf  10700  eldm3  35943  elima4  35958  brsset  36069  brbigcup  36078  elfix2  36084  elfunsg  36096  elsingles  36098  funpartlem  36124  ellines  36334  elhf2g  36358  bj-elpwgALT  37361  cover2g  38037